\begin{tabbing}
World
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$T$:(Id$\rightarrow$Id$\rightarrow$Type)\+
\\[0ex]$\times$${\it TA}$:(Id$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$$M$:(IdLnk$\rightarrow$Id$\rightarrow$Type)
\\[0ex]$\times$($i$:Id$\rightarrow\mathbb{N}\rightarrow$($x$:Id$\rightarrow$$T$($i$,$x$)))
\\[0ex]$\times$($i$:Id$\rightarrow\mathbb{N}\rightarrow$Action(w{-}action{-}dec(${\it TA}$;$M$;$i$)))
\\[0ex]$\times$($i$:Id$\rightarrow\mathbb{N}\rightarrow$(\{$m$:Msg($M$)$\mid$ source(mlnk($m$)) $=$ $i$ \} List))
\\[0ex]$\times$($i$:Id$\rightarrow$w{-}automaton($T$($i$);${\it TA}$($i$);$M$))
\\[0ex]$\times$Top
\-
\end{tabbing}